A, B:Type, f, g:(A(B + Top)), x:A.
(can-apply([f?g];x))  ((can-apply(f;x))  (can-apply(g;x))) 

latex

ProofTree

Definitions	Type, t  T, Top, left + right, x:AB(x), x:A. B(x), f(a), isl(x), b, , P  Q, if b then t else f fi , P  Q, P  Q, False, A, {T}, Dec(P), case b of inl(x) => s(x) | inr(y) => t(y), x:A  B(x), P & Q, P  Q, can-apply(f;x), [f?g], b, , s = t, SQType(T), s ~ t, Unit
Lemmas	bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, decidable assert, ifthenelse wf, assert wf, isl wf, top wf